Termination proof of /tmp/tmp3ABePw/Ex15

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))

The replacement map contains the following entries:

and: {1}
true: empty set
false: empty set
if: {1}
add: {1}
0: empty set
s: empty set
first: {1, 2}
nil: empty set
cons: empty set
from: empty set

↳ CSR

  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))

The replacement map contains the following entries:

and: {1}
true: empty set
false: empty set
if: {1}
add: {1}
0: empty set
s: empty set
first: {1, 2}
nil: empty set
cons: empty set
from: empty set

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))

The replacement map contains the following entries:

and: {1}
true: empty set
false: empty set
if: {1}
add: {1}
0: empty set
s: empty set
first: {1, 2}
nil: empty set
cons: empty set
from: empty set

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {first, FIRST} are replacing on all positions.
For all symbols f in {and, if, add, AND, IF, ADD} we have µ(f) = {1}.
The symbols in {s, cons, from, U, FROM} are not replacing on any position.

The collapsing dependency pairs are DP_c:

AND(true, X) → X
IF(true, X, Y) → X
IF(false, X, Y) → Y
ADD(0, X) → X

The hidden terms of R are:

add(X, Y)
first(X, Z)
from(s(X))

Every hiding context is built from:

add on positions {1}
first on positions {1, 2}

Hence, the new unhiding pairs DP_u are :

AND(true, X) → U(X)
IF(true, X, Y) → U(X)
IF(false, X, Y) → U(Y)
ADD(0, X) → U(X)
U(add(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
U(add(X, Y)) → ADD(X, Y)
U(first(X, Z)) → FIRST(X, Z)
U(from(s(X))) → FROM(s(X))

The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 5 less nodes.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ QCSDP

              ↳ QCSDPReductionPairProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {first} are replacing on all positions.
For all symbols f in {and, if, add, ADD} we have µ(f) = {1}.
The symbols in {s, cons, from, U} are not replacing on any position.

The TRS P consists of the following rules:

U(add(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
U(add(X, Y)) → ADD(X, Y)
ADD(0, X) → U(X)

The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

Using the order
Polynomial interpretation [25]:

POL(0) = 2
POL(ADD(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(U(x₁)) = 1 + 2·x₁
POL(add(x₁, x₂)) = 2 + x₁ + x₂
POL(cons(x₁, x₂)) = x₂
POL(first(x₁, x₂)) = 1 + x₁ + x₂
POL(from(x₁)) = 1 + 2·x₁
POL(nil) = 2
POL(s(x₁)) = x₁

the following usable rules

add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))

could all be oriented weakly.
Furthermore, the pairs

U(add(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
U(add(X, Y)) → ADD(X, Y)
ADD(0, X) → U(X)

could be oriented strictly and thus removed.
All pairs have been removed.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ QCSDP

              ↳ QCSDPReductionPairProof

                ↳ QCSDP

                  ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {first} are replacing on all positions.
For all symbols f in {and, if, add} we have µ(f) = {1}.
The symbols in {s, cons, from} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.